Inference at * 1 
Iof proof for Lemma do-apply-p-lift:



1. A : Type
2. B : Type
3. P : A
4. d : x:ADec(P(x))
5. f : {x:A| P(x)} B
6. x : A
  (isl(case d(x) of inl(a) => inl (f(x))  | inr(a) => inr a ))
   (outl(case d(x) of inl(a) => inl (f(x))  | inr(a) => inr a ) = f(x)) 

latex

 by ((((GenConclAtAddr [1;1;1;1]) 
CollapseTHENA (Auto))) 
CCollapseTHEN (((D (-2)) 

CCoCollapseTHEN (((Reduce 0) 
CCollapseTHEN (Auto)))))) 

latex

CC.

Definitions	x:A. B(x), P  Q, left + right, inl x , True, b, {x:A| B(x)} , outl(x), P  Q, , Dec(P), x(s), f(a), inr x , A, x:AB(x), Type, False, t  T, s = t
Lemmas	decidable wf, true wf, false wf